#ifndef _REDUCT_PERCEPTION_RULES_H
#define _REDUCT_PERCEPTION_RULES_H

#include "ComboReduct/reduct/reduct.h"
#include "ComboReduct/combo/type_tree.h"

namespace reduct {
  
  //add in the set of assumptions such knowledge
  //f(x, z) <= max{d(x, y), d(y, z)}
  //when encounting f(x, y) and f(y, z) and d is ultrametric
  struct reduce_ultrametric : public crule<reduce_ultrametric> {
    void operator()(vtree& tr,vtree::iterator it) const;
  };
 
  //add in the set of assumptions such knowledge
  //f(x, z)
  //when encounting f(x, y) and f(y, z)
  struct reduce_transitive : public crule<reduce_transitive> {
    void operator()(vtree& tr,vtree::iterator it) const;
  };

  //reduce f(x,x) -> true iff f is reflexive
  struct reduce_reflexive : public crule<reduce_reflexive> {
    void operator()(vtree& tr,vtree::iterator it) const;
  };

  //reduce f(x,x) -> false iff f is irreflexive
  struct reduce_irreflexive : public crule<reduce_irreflexive> {
    void operator()(vtree& tr,vtree::iterator it) const;
  };


  //add f(y,x) in the set of assumptions if f(x,y)
  //Note that although it seems that since a symmetric
  //operator is commutative there is no need of this rule
  //it is not true because this rule permits to combines
  //different properties of a relation, as for instance
  //if the relation is both symmetric and transitive
  //then the combination of reduce_transitive and
  //reduce_symmetric can permit more reductions
  //than with associative reduction.
  struct reduce_symmetric : public crule<reduce_symmetric> {
    void operator()(vtree& tr,vtree::iterator it) const;
  };


  //reduce f(x,y) -> 0 iff f verifies the property of identity of indiscernibles
  struct reduce_identity_of_indiscernibles : public crule<reduce_identity_of_indiscernibles> {
    void operator()(vtree& tr,vtree::iterator it) const;
  };

}

#endif
